package org.andes.base;

import java.util.List;

import org.andes.kownledge.operator.Constant;
import org.andes.kownledge.operator.Key;
import org.andes.kownledge.operator.Num;
import org.andes.kownledge.operator.Predication;
import org.andes.kownledge.operator.Term;
import org.andes.kownledge.operator.Variable;
import org.andes.kownledge.operator.func.Func;
import org.armedbear.lisp.Cons;
import org.armedbear.lisp.LispObject;
import org.armedbear.lisp.Symbol;

public class Unification {

	
	///; -*- Mode: Lisp; Syntax: Common-Lisp -*-
	// Unification.cl
	// This code is from Peter Norvig's book; Paradigms of AI programming.  
	// This code was downloaded from: ftp.mkp.com/pub/Norvig on 08/02/2000 
	// and is based upon the files patmatch.lisp, Prolog1.lisp and 
	// unify.lisp. 
	/// Copyright (c) 1991 Peter Norvig
	/// Modifications by Anders Weinstein 2002-2008
	/// Modifications by Brett van de Sande, 2005-2008

	//(load "c:/SolutionGraph/Utility.cl")

	//(package "Unification")

	//================================================================
	// Constants and parameters

//	(defconstant fail nil "Indicates pat-match failure")
//
//	//sbcl has problems with defconstant, see "sbcl idiosyncracies"
//	(#-sbcl defconstant #+sbcl sb-int:defconstant-eqx 
//		no-bindings '((t . t))
//		#-sbcl "Indicates pat-match success, with no variables."
//		#+sbcl #'equalp)
	
//
//	(defvar *occurs-check* t "Should we do the occurs check?")


	//==================================================================
	// Pattern matching functions.


//	(defun pat-match (pattern input &optional (bindings no-bindings))
//	  "Match pattern against input in the context of the bindings"
//	  (cond ((eq bindings fail) fail)
//	        ((variable-p pattern)
//	         (match-variable pattern input bindings))
//	        ((eql pattern input) bindings)
//	        ((segment-pattern-p pattern)                
//	         (segment-matcher pattern input bindings))  
//	        ((single-pattern-p pattern)                 ; ***
//	         (single-matcher pattern input bindings))   ; ***
//	        ((and (consp pattern) (consp input)) 
//	         (pat-match (rest pattern) (rest input)
//	                    (pat-match (first pattern) (first input) 
//	                               bindings)))
//	        (t fail)))
	public void pat_macth(){
		
	}

//	(defun variable-boundp (v Bindings)
//	  "Has the variable x been bound already in the bindings."
//	  (and (variable-p v)
//	       (member v Bindings :test #'equalp :key #'car)))
	public void variable_boundp(){
		
	}

//	(defun variable-p (x)
//	  "Is x a variable (a symbol beginning with `?')?"
//	  (and (symbolp x) (equal (char (symbol-name x) 0) #\?)))
	public static boolean variable_p(LispObject x){
		if(x instanceof Symbol){
			return ((Symbol)x).getName().startsWith("?");
		}
		else
			return false;
		
		
	}


//	(defun variables-in (exp)
//	  "Return a list of all the variables in EXP."
//	  (unique-find-anywhere-if #'variable-p exp))
	public static LispObject variable_in(LispObject exp){
		if(exp.SYMBOLP()==Symbol.T&&variable_p((Symbol)exp)){
			Symbol result=new Symbol(((Symbol)exp).getName());
			return result;
		}else if(exp instanceof Cons){
			Cons result=new Cons(variable_in(exp.car()),variable_in(exp.cdr()));		
			return result;
		}
		return null;
			
		
	}


//	(defun rename-variables (x)
//	  "Replace all variables in x with new ones."
//	  (sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))
//	                  (variables-in x))
//	          x))
	
//	public static LispObject rename_variable(LispObject exp){
//		if(exp.SYMBOLP()==Symbol.T){
//			if(variable_p((Symbol)exp)){
//				Symbol result=new Symbol(((Symbol)exp).getName()+auxiliary.makeNum());
//				return result;
//			}else if(exp==Nil.NIL){
//				return Nil.NIL;
//				
//			}else{
//				Symbol result=new Symbol(((Symbol)exp).getName());
//				return result;
//			}			
//		}else if(exp instanceof Cons){
//			Cons result=new Cons(rename_variable(exp.car()),rename_variable(exp.cdr()));		
//			return result;
//		}
//		return exp;
//					
//	}
//	public static Predication rename_variable(Predication pred){
//		Predication result=new Predication();
//		result.setPredicate(pred.getPredicate());
//		for(Term term:pred.getArguments()){
//			if(term instanceof Variable){
//				Variable var=(Variable)term;
//				String name=var.getName()+auxiliary.makeNum();
//				Variable var2=new Variable(name);
//				result.addArgument(var2);
//			}else if(term instanceof Key){
//				Key key=(Key)term;
//				Term value=key.getValue();
//				Key key2=new Key(key.getType());
//				key2.setValue(key.getValue());
//				if(value instanceof Variable){
//					Variable var=(Variable)value;
//					String name=var.getName()+auxiliary.makeNum();
//					Variable var2=new Variable(name);
//					key2.setValue(var2);
//				}								
//				result.addArgument(key2);
//			}else if(term instanceof Func){
//				
//			}
//			
//		}
//		
//		return result;
//					
//	}


	///;
	///; ============= test if expression contains variables ====================
	///;

//	(defun groundp (form)
//	  "True if the given form contains no variables"
//	  (cond ((variable-p form) NIL)
//		((atom form) t)
//		(t (and (groundp (car form))
//			(groundp (cdr form))))))
//	public static boolean groundp(LispObject form){
//		if(variable_p(form))
//			return false;
//		else if(form.atom())
//			return false;
//		return groundp(form.car())&&groundp(form.cdr());
//		
//	}
	public static boolean groundp(Object form){
		if(form instanceof Variable)
			return false;
		else if(form instanceof Predication){
			for(Term term:((Predication)form).getArguments()){
				if(term instanceof Variable)
					return false;
				
			}
			return true;
		}
			return false;
		
	}
//	(defun ground-expression (form bindings)
//	  "If all the variables in the given form are bound, 
//	   returns a ground instance of it. Otherwise, returns NIL"
//	  (and (all-boundp form bindings)
//	       (subst-bindings bindings form)))

//	(defun all-boundp (form bindings)
//	  "True if the given form's variables all have bindings"
//	  (cond ((variable-p form)
//		 (get-binding form bindings))
//		((atom form) t)
//		(t (and (all-boundp (car form) bindings)
//			(all-boundp (cdr form) bindings)))))
	
	
	
	
	
//	(defun subst-bindings (bindings x)
//	  "Substitute the value of variables in bindings into x,
//	  taking recursively bound variables into account."
//	  (cond ((eq bindings fail) fail)
//	        ((eq bindings no-bindings) x)
//	        ((and (variable-p x) (get-binding x bindings))
//	         (subst-bindings bindings (lookup x bindings)))
//	        ((atom x) x)
//		// remove null keyword pairs
//		((and (valid-keyword-pair x)
//		      (null (subst-bindings bindings (cadr x))))
//		 (subst-bindings bindings (cddr x)))
//	        (t (reuse-cons (subst-bindings bindings (car x))
//	                       (subst-bindings bindings (cdr x))
//	                       x))))
	
	public static Object subst_bindings(Bindings binds,Object x){
		if(x instanceof Variable){
			return subst_bindings(binds,binds.get_binding((Variable)x));
		}else if(x instanceof Func){
			return ((Func)x).substBindings(binds);
		}
		else
			return x;			
		
	}


	///; ================================================================== 
	///;                              Unification
	///; ================================================================== 

//	(defun unify (x y &optional (bindings no-bindings) test test-function)
//	  "See if x and y match with given bindings."
//	  (cond ((eq bindings fail) fail)
//	        ((eql x y) bindings)
//		// allow 1.0 and 1 to match
//		((and (numberp x) (numberp y) (= x y)) bindings)
//	        ((variable-p x) (unify-variable x y bindings))
//	        ((variable-p y) (unify-variable y x bindings))
//		// this allows for arbitrary matching functions
//		((and test (funcall test x) (funcall test y)) 
//		 (funcall test-function x y bindings))
//		// handle orderless objects
//		((and (orderless-p x) (orderless-p y)) 
//		 (unify (order-expr (cdr x) #'orderless-sort bindings) 
//			(order-expr (cdr y) #'orderless-sort bindings) 
//			bindings test test-function))
//		// handle symmetry under cyclic permutations
//		((and (cyclic-p x) (cyclic-p y)) 
//		 (unify (order-expr (cdr x) #'cyclic-sort bindings) 
//			(order-expr (cdr y) #'cyclic-sort bindings) 
//			bindings test test-function))
//		// Match any keyword pairs; only compare keyword pair against 
//		// a proper list.  
//		((and (valid-keyword-pair x) (listp y) (null (cdr (last y))))
//		 (unify-keyword x y bindings))
//		((and (valid-keyword-pair y) (listp x) (null (cdr (last x))))
//		 (unify-keyword y x bindings))
//		// Then test that at least one order did work.
//		((or (valid-keyword-pair x) (valid-keyword-pair y)) 
//		 (error "Can't unify keyword pairs in ~S~%     and ~S~%" x y)) 
//		// Recursion for cons
//	        ((and (consp x) (consp y))
//		 (unify (rest x) (rest y) 
//				 (unify (first x) (first y) 
//					bindings test test-function) 
//				 test test-function))
//	        (t fail)))
	
	public static Bindings unify(Object x,Object y,Bindings bindings){
		if(x.equals(y))
			return bindings;
		else if(x instanceof Constant&&y instanceof Constant){
			if( ((Constant)x).getValue().equals(((Constant)y).getValue()))
				return bindings;		
		}else if(x instanceof Num&&y instanceof Num){
			if( ((Num)x).getValue()==((Num)y).getValue())
				return bindings;		
		}
		else if(x instanceof Integer&&y instanceof Integer){
			int xint=((Integer)x).intValue();
			int yint=((Integer)x).intValue();
			if(xint==yint)
				return bindings;
			else
				return null;
		}
		else if(x instanceof Key){
			return unify(((Key)x).getValue(),y,bindings);			
		}else if(y instanceof Key){
			return unify(x,((Key)y).getValue(),bindings);			
		}	
		else if(x instanceof Variable){
			return unify_variable((Variable)x,y,bindings);			
		}else if((x instanceof Symbol)&&(y instanceof Symbol)&&(((Symbol)x).getName().equalsIgnoreCase(((Symbol)y).getName()))){
			return bindings;
		}
		else if(y instanceof Variable){
			return unify_variable((Variable)y,x,bindings);
			
		}else if (x instanceof Predication&&y instanceof Predication){
			return unify_predication((Predication)x,(Predication)y,bindings);
							
		}else if (x instanceof Func&&y instanceof Func){
			return unify_func((Func)x,(Func)y,bindings);
		}
		
		return null;
	}
	                       
	private static Bindings unify_func(Func xp, Func yp,Bindings bindings) {
		List<Term> xparas=xp.getVar();
		List<Term> yparas=yp.getVar();
		if(!xp.getFuncName().equalsIgnoreCase(yp.getFuncName()))
			return null;
		
		if(xp.getVar().size()!=yp.getVar().size()){
			return null;
		}
		
		for(int i=0;i<xparas.size();i++){
			
			bindings=unify(xparas.get(i),yparas.get(i),bindings);
			if(bindings==null)
				return null;
			
		}		
		return bindings;
	}

	public static Bindings unify_predication(Predication xp,Predication yp,Bindings bindings){
		List<Term> xparas=xp.getArguments();
		List<Term> yparas=yp.getArguments();
		List<String> xkeys=xp.getKeys();
		List<String> ykeys=yp.getKeys();
		if(!xp.getPredicate().equalsIgnoreCase(yp.getPredicate()))
			return null;
		
		if(xp.getArguments().size()!=yp.getArguments().size()){
			return null;
		}
//		if(xkeys.size()!=ykeys.size()){
//			return null;
//		}
		for(int i=0;i<xparas.size();i++){
			
			bindings=unify(xparas.get(i),yparas.get(i),bindings);
			if(bindings==null)
				return null;
			
		}
		for(String key:xkeys){
			Term xValue=xp.getKeyValue(key);
			Term yValue=yp.getKeyValue(key);	
			if(yValue!=null){
				bindings=unify(xValue,yValue,bindings);
				if(bindings==null)
					return null;
			}						
		}
		for(String key:ykeys){
			Term xValue=xp.getKeyValue(key);
			Term yValue=yp.getKeyValue(key);	
			if(xValue!=null){
				bindings=unify(yValue,xValue,bindings);
				if(bindings==null)
					return null;
			}
			
			
		}
		return bindings;
		
	}
	                       
//	(defun unify-variable (var x bindings)
//	  "Unify var with x, using (and maybe extending) bindings."
//	  (cond ((get-binding var bindings)
//	         (unify (lookup var bindings) x bindings))
//	        ((and (variable-p x) (get-binding x bindings))
//	         (unify var (lookup x bindings) bindings))
//	        ((and *occurs-check* (occurs-check var x bindings))
//	         fail)
//	        (t (extend-bindings var x bindings))))
//	public static Bindings unify_variable(LispObject var,LispObject x,Bindings bindings){
//		if(bindings==null)
//			System.out.println("bindings==null");
//		if(bindings.get_binding(var)!=null){
//			return unify(bindings.lookup(var),x,bindings);
//		}else if(variable_p(x)&&(bindings.get_binding(x)!=null)){
//			return unify(var,bindings.lookup(x),bindings);			
//		}else
//			return bindings.extend_bindings(var, x);
//		
//	}
	public static Bindings unify_variable(Variable var,Object x,Bindings bindings){
		if(bindings==null)
			System.out.println("bindings==null");
		if(bindings.get_binding(var)!=null){
			return unify(bindings.lookup(var),x,bindings);
		}else if(x instanceof Variable&&(bindings.get_binding((Variable)x)!=null)){
			return unify(var,bindings.lookup((Variable)x),bindings);			
		}else
			return bindings.extend_bindings(var, x);
		
	}

//	(defun occurs-check (var x bindings)
//	  "Does var occur anywhere inside x?"
//	  (cond ((eq var x) t)
//	        ((and (variable-p x) (get-binding x bindings))
//	         (occurs-check var (lookup x bindings) bindings))
//	        ((consp x) (or (occurs-check var (first x) bindings)
//	                       (occurs-check var (rest x) bindings)))
//	        (t nil)))

//	(defun exactly-equal (x y)
//	  "test equality under unification without any bindings"
//	  (equal (unify x y) no-bindings))

	///
	///                    Match to keywords pairs
	///
	///  Keywords pairs may occur in any order in a list.  One may
	///  optionally specify a default value
	///  The format is 
	///       :keyword value [default]
	///  If there is no match, value is bound to default or nil
	///

//	(defun valid-keyword-pair (x)
//	  "Check x is list starting with a keyword and value."
//	  (and (consp x) (keywordp (car x)) (consp (cdr x))))
	public boolean valid_keywor_pair(LispObject x){
		if(x instanceof Cons)
			return (x.car().toString().equals(":keyword")&&(x.cdr() instanceof Cons));
		else 
			return false;
		
	}

//	(defmacro get-any-default-value (x)
//	  "Remove any non-keyword from beginning of x"
//	  `(when (and (consp ,x) (not (keywordp (car ,x)))) (pop ,x)))

//	(defun unify-keyword (x y bindings)
//	  "Find match in y for first keyword pair in x; y must be a proper list."
//	  // keyword pair is removed from x:
//	  (let* ((ykey (member (pop x) y)) (var (pop x))
//		 // remove any default value from x
//		 (default (get-any-default-value x)))
//	    (cond
//	     // if value in x is nil, just remove keyword pair
//	     ((null var) (unify x y bindings))
//	     // if keyword pair is in y, match values:
//	     ((consp (cdr ykey))	;Is there a keyword and value in y?
//	      (let ((post (cddr ykey)))
//		(get-any-default-value post)	;discard any default value from y
//		(unify x (append (ldiff y ykey) post) ;keyword pair removed
//		       // if y value is nil, bind to default instead
//		       (unify var (or (second ykey) default) bindings))))
//	     // no match:  bind var to default
//	     (t (unify x y (unify var default bindings))))))


	// valid expressions include:  (symmetry-type a b c ...)
	//                             (symmetry-type . ?a)
	//                             (symmetry-type ?a)      


//	(defun order-expr (x sort-function bindings)
//	  "handle any variables when ordering a list according to symmetry-type"
//	  (cond 
//	   ((variable-p x) x)                 ;(symmetry-type . ?a)
//	   ((and (listp x) (null (cdr x))) x) ;(symmetry-type ?a)
//	   // (orderless a b c ...)
//	   ((and (listp x) (null (cdr (last x)))) ;check for proper list
//	    // Sort everything before any keywords
//	    (let ((keywords (member-if #'keywordp x)))
//	      (nconc 
//	       (funcall sort-function 
//			(copy-list (subst-bindings bindings (ldiff x keywords))))
//		 keywords)))
//	   (t (error "Invalid list ~S.~%  Need a proper list with all variables bound." 
//		     x))))

	/// Orderless lists with (orderless ...)

//	(defun orderless-p (x)
//	  (and (consp x) (eq (car x) 'orderless)))
//
//	(defun orderless-sort (x) (sort x #'expr<))

	/// Symmetry under cyclic permutations with (cyclic ...)

//	(defun cyclic-p (x)
//	  (and (consp x) (eq (car x) 'cyclic)))

	// use (setf *print-circle* t) to debug
//	(defun cyclic-sort (x)
//	  "canonical order under cyclic permutations using expr<, destructive"
//	  (let ((lx (length x)) (best x))
//	    (setf (cdr (last x)) x) ;make circular list
//	    (do ((y (cdr x) (cdr y))) ((eq y x)) // iterate over cyclic permutations
//		(when (circular-expr< y best lx) (setf best y))) ;compare with best
//	    (setf (cdr (nthcdr (- lx 1) best)) nil)    ;undo circular list
//	    best))

//	(defun circular-expr< (a b n)
//	  "version of expr< for use with circular lists"
//	  (cond ((< n 1) nil)
//		((expr< (car a) (car b)) t)
//		((expr< (car b) (car a)) nil)
//		((circular-expr< (cdr a) (cdr b) (- n 1)))))

	/// ===========================================================================

//	(defun unify-with-list (i L &optional (Bindings No-Bindings))
//	  "Attempt to unify item i with some element in list L returning all 
//	   possible unifications."
//	  (loop for i2 in L
//	      when (unify i i2 Bindings)
//	      collect it))

	//////////////////////////////////////////////////////////////////////////////;
	// filter-values
	// Search through a list of expressions and pull out the subset of each 
	// expression that are accepted by the filter.
	//
	// Arguments: Filter: The filter expression to be used.
	//            Exps:   The expressions to be filtered.
	//     &optional
	//             Bindings:  An optional set of bindings to use.

//	(defun filter-expressions (Filter Exps &optional (Bindings no-bindings))
//	  (remove-if-not #'(lambda (e) (unify e filter bindings)) Exps))

	////////////////////////////////////////////////////////////////////////;
	// generate-bindings
	// Given a list of variables and a list of matching bindings generate 
	// a dotted pair style bindings list from the two.
	//
	// This is used with the Operator-Variables and OpApp-Values elements.
	//
	// Arguments:
	//   Vars: A list of variables to be matched.
	//   Vals: The list of values to be matched with them.
	//
	// Returns: The result of matching the variables and values.

//	(defun generate-bindings (Vars Vals)
//	  "Obtain a list of bindings for the qual listf of vars and vals."
//	  
//	  (if (not (equal (length Vars)
//			  (length Vals)))
//	      (error "Incompatable Variable/Value lists supplied to generate-bindings. ~A ~A" Vars Vals)
//	  
//	    (mapcar #'cons Vars Vals)))


	//=============================================================================
	// Code by Kurt VanLehn.

	/// the regular subst-bindings is recursive, but we only want the top level 
	/// value to have a quote around it.  For instance, if ?x is bound to ?y which 
	/// is bound to 5, then we want (mod ?x 90) to become (mod '5 90).  Thus at the
	/// first occurance in the cons-tree walk of a variable, we switch from this 
	/// function to the regular subst-bindings function (KVL)

//	(defun subst-bindings-quoted (bindings x &key unground-ok)
//	  "Returns x with all variables inside a quote, ready for eval'ing"
//	  // If bindings equals no-bindings, we still need to test for 
//	  // unground variables.
//	  (cond ((eq bindings fail) fail)
//	        ((variable-p x)
//		 (let ((y (subst-bindings bindings x)))
//		   (if (or unground-ok (groundp y))
//		       (list 'quote y)
//		       (error "subst-bindings-quoted unground expression ~A" y))))
//		((atom x) x)
//		// Just substitute in variables, allowing ungrounded expressions
//		((eq (car x) 'quote) (subst-bindings bindings x))
//		// allow lisp expression to test for variables or report errors
//		((member (car x) '(groundp error warn)) 
//		 (reuse-cons (car x)
//			     (subst-bindings-quoted bindings (cdr x) :unground-ok t)
//			     x))
//	        (t (reuse-cons (subst-bindings-quoted bindings (car x) 
//						      :unground-ok unground-ok)
//			       (subst-bindings-quoted bindings (cdr x)
//						      :unground-ok unground-ok)
//			       x))))
//	public static LispObject subst_bindings_quoted(Bindings bindings,Object x,boolean unground_ok) throws Error{
//		if(x instanceof Variable){
//			LispObject y=subst_bindings(bindings,(Variable)x);
//			if(unground_ok||groundp(y)){
//				Symbol s=new Symbol("quote");
//				Cons result=new Cons(new Cons(s),x);
//				return result;
//				
//			}else
//				throw new Error();
//						
//		}else if(x.atom()){
//			return x;
//			
//		}else if(x.car().getStringValue().equals("quote")){
//			return subst_bindings(bindings,x);
//		}else if((x.car() instanceof Symbol)&&((Symbol)x).getName().equals("groundp")
//				&&((Symbol)x).getName().equals("error")
//				&&((Symbol)x).getName().equals("warn")){
//			return null;
//			
//		}else{
//			LispObject obj1=subst_bindings_quoted(bindings,x.car(),unground_ok);
//			LispObject obj2=subst_bindings_quoted(bindings,x.car(),unground_ok);
//			//return auxiliary.resue_cons(obj1,obj2,x);
//			return new Cons(obj1,obj2);//?
//		}
//		
//		
//	}


	//=============================================================================
	// Code by Collin Lynch

	/// We may want to perform recursive binds or more complex binds in which 
	/// case it will become necessary to call some function for each element to 
	/// be bound.  
	/// Subst-bindings-func does so by calling the specified predicate function 
	/// and setting its value in the location specified.

//	(defun subst-bindings-func (Bindings Func X)
//	   "Returns X with all variables inside replaces by the value of Func(B)."
//	  (cond ((eq bindings fail) fail)
//	        ((eq bindings no-bindings) x)
//	        ((variable-p x)
//		 (funcall Func (subst-bindings Bindings (lookup x bindings))))
//	        ((atom x) x)
//	        (t (cons (subst-bindings-func bindings Func (car x))
//	                 (subst-bindings-func bindings Func (cdr x))))))



	/// Given a list of elements this code collects up all those members of
	/// the list that unify with the supplied pattern.  Otional keywoyd arguments
	/// can be supplied for key and bindings if any.

//	(defun collect-unifiers (set pattern &key (bindings no-bindings) 
//						  (key #'identity))
//	  "collect all of the expressions that unify with the pattern in set."
//	  (remove-if-not 
//	   #'(lambda (x)
//	       (unify (funcall key x) 
//		      pattern bindings))
//	   set))
	  

	/// given a format spec in need of unification and bindings
	/// substitute the bindings into it and call format on the
	/// results.
//	(defun format-subst (form bindings)
//	  "Apply format to the result of binding the elements."
//	  (apply 'format (cons nil (subst-bindings bindings form))))

	///; ==================================================================
	///; Strip off the leading question mark from a variable

//	(defun strip-variable-qm (var)
//	  "Get back the symbol for the var sans the quote mark."
//	  (if (not (variable-p var))
//	      (error "Non-var supplied to strip-variable-qm.")
//	    (intern (string-upcase (subseq (format nil "~a" var) 1)))))

//	(defun strip-expression-var-qms (exp)
//	  "Apply strip-variable-qm to all vars in exp."
//	  (cond ((null exp) ())
//		((variable-p (car exp))
//		 (cons (strip-variable-qm (car exp))
//		       (strip-expression-var-qms (cdr exp))))
//		((listp (car exp)) 
//		 (cons (strip-expression-var-qms (car exp))
//		       (strip-expression-var-qms (cdr exp))))
//		(t (cons (car exp) (strip-expression-var-qms (cdr exp))))))


	/// Cycle through all of the variables in the expression replacing them
	/// with an upper-case string form sans question mark.
//	(defun strip-replace-exp-vars (exp)
//	  "Apply strip-variable-qm to all vars in exp."
//	  (cond ((null exp) ())
//		((variable-p exp) (list (string-upcase 
//					 (subseq (format nil "~w" exp) 1)) ))
//		((atom exp) (list exp))
//		((variable-p (car exp))
//		 (cons (string-upcase (subseq (format nil "~w" (car exp)) 1)) 
//		       (strip-replace-exp-vars (cdr exp))))
//		((listp (car exp))
//		 (cons (strip-replace-exp-vars (car exp))
//		       (strip-replace-exp-vars (cdr exp))))
//		(t (cons (car exp) (strip-replace-exp-vars (cdr exp))))))


	///; =======================================================================
	///; Non-destrictively modify bindings
	///; Given a list of bindings we may want to modify them by either removing 
	///; a variable binding or replacing an existing binding with a new one.
	///; This code does so.

	/// Given a list of bindings remove a variable binding
	/// from it (by variable) if it exists.
//	(defun reduce-bindings (Var Bindings)
//	  "Remove the variable from bindings if it is there."
//	  (remove Var Bindings :key #'car))


	/// Given a list of bindings change the binding for a specified
	/// var from its current value to the supplied value. (nondestructive)
	/// But change it only if the variable already has a value.
//	(defun change-bindings (Var Value Bindings)
//	  "Change the bindings value for var from its initial form the new one."
//	  (when (get-binding Var Bindings)
//	    (extend-bindings Var Value (reduce-bindings Var Bindings))))


//	#| Unused for now.
	/// One expression (containing variables) subsumes another if:
	/// 1. They are of the same length and
	/// 2. All positions that contain bound constants in one 
	///    expression contain identical bound constants in the
	///    other and
	/// 3. If there exist any unbound variables within the
	///    subsuming expression then at least one of the
	///    corresponsing locations in the subsumed expression
	///    is bound.
	///
	/// Therefore foo(a ? c) subsumes foo(a x c) but not 
	/// foo(a ? ?)
	///
	/// This is a recursive process of testing.

//	(defun expression-subsumes? (subsumer subsumed &optional (bindings no-bindings))
//	  "Does the subsumer subsume the subsumed?"
//	  (declare (optimize (speed 0)))
//	  (cond ((eq bindings NIL) NIL)
//		((eql subsumer subsumed) bindings)
//		//((and (variable-p subsumer) (variable-p subsumed)) bindings)
//		((and (consp subsumer) (consp subsumed)) 
//		 (pprint (LIST subsumer subsumed))
//		 (expression-subsumes? 
//		  (cdr subsumer) (cdr subsumed)
//		  (expression-subsumes? 
//		   (car subsumer) (car subsumed) bindings)))
//		(t nil)))
//	|#








}
